The sheer complexity of the software development process makes it increasingly difficult for programmers to detect programming flaws. As a result, software testing has become an important part of software development.
Software can be tested by a human tester who executes the software and monitors its progress. However, as the complexity of the software increases, it becomes virtually impossible for a person to reproduce all possible execution scenarios in a reasonable amount of time. Therefore, testers can build a model of the software to model (e.g., simulate) execution of the software. Because modeling allows automated exploration of the software, it can perform a more extensive analysis than what is possible by human analysts.
One technique for modeling software is procedure summarization. Procedure summaries can represent a summarization of calculations done in software. In this way, calculations during modeling can be simplified, and more efficient modeling of execution can be performed.
For example, if during execution, the software has state s when it enters a procedure P and state s′ when it exits the procedure, a summary of the procedure can include the following state pair:                (s,s′)        
In practice, the summary of a procedure contains such a state pair if in state s there is an invocation of P that yields the state s′ on termination. Thus, the summary can include plural state pairs, one for each possible pair of initial state and resulting states. The procedure summary can be used in place of executing the procedure during modeling.
Procedure summaries have been used with success for sequential programs. However, for multithreaded software, some of the state variables may be shared by multiple threads. Thus, conventional procedure summaries are of little use. For example, during execution of the procedure, updates to shared state variables may be performed by interleaved actions of concurrently executing threads. Such actions may depend on the local states of the other threads. Therefore, the state pairs do not accurately reflect the possible resulting states in a multithreaded execution scenario.
So, there still exists a need for improving procedure summary technology.